﻿/************************************************************************
 * SMLib - State Model Library
 * Copyright (C) 2012-2013 Ali Khalili (khalili_DOT_ir_@SIGN_gmail_DOT_com)
 * **********************************************************************
 * This program is free software; you can redistribute it and/or modify it
 * under the terms of the GNU Lesser General Public License (LGPL) published 
 * by the Free Software Foundation; either version 2.1 of the License, or (at your
 * option) any later version. This program is distributed without any
 * warranty. See the GNU Lesser General Public License for more details. 
 * ***********************************************************************
 * File         :     SMLib\Automata\IA\InterfaceAutomaton.cs
 * Description  :     Implementation of Input-Output Labeled Transition System Automata
 * Change log   :     -12 March 2013:  Add features
 * To Do        :     -[make type of steps compatible with alphabet]
 * 						replace it with STEP
 ************************************************************************/
//#define VISUALIZATION_ENABLED
using System;
using System.Collections.Generic;
using System.Text;
using SMLib.Automata.Base;
using SMLib.Utils;
using SMLib.Base;
using SMLib.Interoperability.DOT;

namespace SMLib.Automata.IA
{
	/// <summary>
	/// When an action execution called but the action is not enabled in the current state
	/// </summary>
	public class NotEnabledActionException : Exception
	{
		//* Nothing
		public NotEnabledActionException (string msg)
		{

		}
	}

	/// <summary>
	/// This exception happen when after giving an input, we realize that there was an output happened just before the input
	/// </summary>
	public class NotValidTraceException : Exception
	{
		/// <summary>
		/// Construction
		/// </summary>
		/// <param name="msg"></param>
		public NotValidTraceException (string msg)
		{

		}
	}

	/// <summary>
	/// Input Output Labeled Transition System (IA), to implement ioco theory
	/// </summary>
	public class InterfaceAutomaton :
        //TranSys<InterfaceAutomaton.IA_State, InterfaceAutomaton.IA_Step>
    	DiGraph<InterfaceAutomaton.IA_State,InterfaceAutomaton.IA_Step>
	{
		Alphabet inputAlphabet;
		//, outputAlphabet;
		public InterfaceAutomaton ()
		{
			inputAlphabet = new Alphabet ();
		}
		#region Definition of State
		/// <summary>
		/// A state in IA
		/// </summary>
		public class IA_State : //IStateContainer//: 
            IState<IA_Step>
		{
			int id;
			List<IA_Step> transitions;

			/// <summary>
			/// Type of states
			/// </summary>
			public enum StateType
			{
				/// <summary>
				/// Active states (enabled to perform controllable actions)
				/// </summary>
				ACTIVE,
				/// <summary>
				/// Passive states (waiting for observable events)
				/// </summary>
				PASSIVE,
				/// <summary>
				/// It can be active or passive
				/// </summary>
				BOTH,
				/// <summary>
				/// If the state doesn't have any transition!
				/// </summary>
				NONE
			}

			/// <summary>
			/// Status of the state:
			/// <list type="">
			/// <item> Active: if it has just inputs or input/outputs (IPairSymbol)</item>
			/// <item> Passive: if it has just outputs</item>
			/// <item> Both: if it has both outputs and inputs (or input/outpus)</item>
			/// <item> None: if it doesn't have any edge</item>
			/// </list>
			/// </summary>
			public StateType Status {
				get {
					StateType myType = StateType.NONE;

					//* if the state doesn't have any transitions!
					if (transitions.Count == 0)
						return StateType.NONE;

					if (((InterfaceAutomaton.IA_Step)transitions [0]).StepType == IA_Step.Step_Type.EVENT)
						myType = StateType.ACTIVE;
					else
						myType = StateType.PASSIVE;

					for (int i = 1; i < transitions.Count; i++) {
						//* we just judge based on the first transition 
						if (
                            (((InterfaceAutomaton.IA_Step)transitions [i]).StepType == IA_Step.Step_Type.EVENT && myType == StateType.PASSIVE)
                            ||
							(
                            (((InterfaceAutomaton.IA_Step)transitions [i]).StepType == IA_Step.Step_Type.ACTION || ((InterfaceAutomaton.IA_Step)transitions [i]).StepType == IA_Step.Step_Type.FUNCTION_CALL)
							&& myType == StateType.ACTIVE)
                            )
							return StateType.BOTH;
					}

					return myType;
				}
			}

			public IA_State (int id)
			{
				transitions = new List<IA_Step> ();
				this.id = id;
			}

			public override string ToString ()
			{
				return id.ToString ();
			}
			#region IStateContainer Members
			/// <summary>
			/// Identifier of IA state
			/// </summary>
			public object Identifier {
				get { return id; }
			}

			/// <summary>
			/// List of steps in the state
			/// </summary>
			public List<IA_Step> Transitions {
				get { return transitions; }
			}

			public void AddTransition (IA_Step step)
			{
				if (transitions.Count == 0) {

				}

				transitions.Add (step);
			}

			/// <summary>
			/// The content of state
			/// <remarks>In model based testing tool, it is the state of system (a snapshot representing the
			/// current state of system sy some state variables)</remarks>
			/// </summary>
			public object content {
				get {
					return null;// throw new NotImplementedException(); 
				}
			}
			#endregion
		}
		#endregion
		#region Definition of Transitions
		/// <summary>
		/// A transition in IA
		/// </summary>
		public class IA_Step //: ITransition<IA_State>
		{

			IA_State target;
			Step_Type type;
			object label;

			/// <summary>
			/// Constructor
			/// </summary>
			/// <param name="isControllable">This action is controllable or not (it is observable)</param>
			public IA_Step (ISymbol label, bool isControllable)
			{
				this.label = label;
				if (isControllable) {
					type = Step_Type.ACTION;
				} else {
					type = Step_Type.EVENT;
				}
			}

			/// <summary>
			/// When you have an input-output pair, use this constructor
			/// </summary>
			/// <param name="label">the input-output label</param>
			public IA_Step (PairOfSymbols label)
			{
				this.label = label;
				type = Step_Type.FUNCTION_CALL;
			}

			/// <summary>
			/// Set destination of the transition
			/// </summary>
			/// <param name="dest">destination of the transition</param>
			public void SetDestination (IA_State dest)
			{
				this.target = dest;
			}

			/// <summary>
			/// Label of transition
			/// </summary>
			public object Label {
				get {
					return label;
				}
			}

			/// <summary>
			/// There are two different kinds of transitions: Actions and Events. Actions are
			/// controllable by user. Events are made by the system and are observable by the user.
			/// </summary>
			public enum Step_Type
			{
				/// <summary>
				/// Controllable action
				/// </summary>
				ACTION,
				/// <summary>
				/// Observable event
				/// </summary>
				EVENT,
				/// <summary>
				/// This is a Controllable action and an immediate consequencing observable event (like when you have
				/// a synchroneous immediate function call and return)
				/// </summary>
				FUNCTION_CALL}

			;

			/// <summary>
			/// Type of this step (which could be action or event)
			/// </summary>
			public Step_Type StepType {
				get {
					return type;
				}

			}

			public override bool Equals (object obj)
			{
				if (obj is IA_Step) {
					IA_Step st = (IA_Step)obj;
					return st.label.Equals (label) && st.type.Equals (type);
				}
                //else if (obj is ISymbol)
                //{
                //    ISymbol st = (ISymbol)obj;
                //    return label.Equals(st);
                //}
                //else if (obj is IPairOfSymbols)
                //{
                //    IPairOfSymbols st = (IPairOfSymbols)obj;
                //    return label.Equals(st);
                //}
                else
					return false;
			}

			public override int GetHashCode ()
			{
				return base.GetHashCode ();
			}

			/// <summary>
			/// The string equivalent of the transition (for presentation purpose)
			/// </summary>
			/// <returns>the string value</returns>
			public override string ToString ()
			{
				if (label == null)
					return "NULL";
				//* 
				if (type == Step_Type.ACTION)
					return "?" + label.ToString ();
				else if (type == Step_Type.EVENT)
					return "!" + label.ToString ();
                //*
                else
					return "!?" + label.ToString ();

			}
			#region ITransition Members
			/// <summary>
			/// The target state of this step
			/// </summary>
			public IA_State Destination {
				get { return target; }
			}
			#endregion
		}
		#endregion
		/// <summary>
		/// Input alphabet of IA
		/// </summary>
		public Alphabet InputAlphabet {
			get {
				return inputAlphabet;
			}
		}

		/// <summary>
		/// Calculates the output alphabet.
		/// </summary>
		/// <returns>The output alphabet.</returns>
		public Alphabet CalculateOutputAlphabet ()
		{
			Alphabet outAlphabet;
			outAlphabet = new Alphabet ();
			foreach (IA_State st in this.GetStates())
				foreach (IA_Step tr in st.Transitions) {
					if (tr.StepType != IA_Step.Step_Type.EVENT)
						continue;
					bool found = false;
					foreach (ISymbol sym in outAlphabet.AllSymbols()) {
						if (sym.Equals (tr.Label)) {
							found = true;
							break;
						}
					}
					if (!found)
						outAlphabet.AddSymbol ((ISymbol)tr.Label);
				}
			return outAlphabet;
		}
		/*
		/// <summary>
		/// Gets the output alphabet.
		/// </summary>
		/// <value>
		/// The output alphabet.
		/// </value>
		public Alphabet OutputAlphabet
        {
            get
            {
                return outputAlphabet;
            }
        }
		*/
		public int ComputeNumberOfNondetStates ()
		{
			int n = 0;
			for (int i = 0; i < Size; i++) {
				int k = 0;
				for (int j = 0; j < states[i].Transitions.Count; j++) {
					if (states [i].Transitions [j].StepType == IA_Step.Step_Type.EVENT)
						k++;
					if (k >= 2) {
						n++;
						break;
					}
				}
			}
			return n;
		}
		//        /// <summary>
		//        /// Read an IA from a DOT file
		//        /// <remarks>[Convention: inputs star with "!" and outputs star with "?"]</remarks>
		//        /// </summary>
		//        /// <param name="fileAddress">the location of input file</param>
		//        /// <returns>the IA</returns>
		//        public static InterfaceAutomaton ReadFromDOT1(string fileAddress)
		//        {
		//            InterfaceAutomaton m = new InterfaceAutomaton();
		//            m.inputAlphabet = new Alphabet();
		//            m.outputAlphabet = new Alphabet();
		//            List<string> statesName = new List<string>();
		//
		//            DotFormat dotReader = new DotFormat();
		//            string ilbl;
		//            foreach (DotFormat.DotTransition tr in dotReader.ReadDotFile(fileAddress))
		//            {
		//                ilbl = tr.Label;
		//                IA_Step t = null;
		//                if (tr.Label.StartsWith("?"))
		//                {
		//                    ilbl = ilbl.Substring(1);
		//                    if (!m.inputAlphabet.Contains(new StringSymbol(ilbl)))
		//                        m.inputAlphabet.AddSymbol(new StringSymbol(ilbl));
		//                    t = new IA_Step(new StringSymbol(ilbl), true);
		//                }
		//				/*
		//                else if (tr.Label.StartsWith("!?"))
		//                {
		//                    throw new Exception("Not supported yet!");
		//                }
		//                */
		//				else if (tr.Label.StartsWith("!"))
		//                {
		//                    ilbl = ilbl.Substring(1);
		//                    if (!m.outputAlphabet.Contains(new StringSymbol(ilbl)))
		//                        m.outputAlphabet.AddSymbol(new StringSymbol(ilbl));
		//                    t = new IA_Step(new StringSymbol(ilbl), false);
		//                }
		//				else
		//				{
		//					throw new Exception("Invalid Label!");
		//				}
		//
		//
		//                IA_State srcNode = null, dstNode = null;
		//                int index = 0;
		//                foreach (string n in statesName)
		//                {
		//                    if (n.Equals(tr.Source))
		//                        srcNode = (IA_State)m[index];
		//
		//                    if (n.Equals(tr.Destination))
		//                        dstNode = (IA_State)m[index];
		//
		//                    if (dstNode != null && srcNode != null)
		//                        break;
		//                    index++;
		//                }
		//
		//                if (srcNode == null)
		//                {
		//                    srcNode = new IA_State(m.Size);
		//                    statesName.Add(tr.Source);
		//
		//                    m.states.Add(srcNode);
		//
		//                    if (tr.Destination == tr.Source)
		//                        dstNode = srcNode;
		//                }
		//
		//                if (dstNode == null)
		//                {
		//                    dstNode = new IA_State(m.Size);
		//                    statesName.Add(tr.Destination);
		//
		//                    m.states.Add(dstNode);
		//                }
		//
		//                t.SetDestination(dstNode);
		//                srcNode.Transitions.Add(t);
		//            }
		//            return m;
		//        }
		///// <summary>
		///// Add a state to the interface automata
		///// </summary>
		///// <param name="myState">the state to be added</param>
		//public void AddState(IA_State myState)
		//{
		//    this.states.Add(myState);
		//}

		//#region Override part
		//protected override void UpdateTransition(IStateContainer src, ITransition tr, object newTr)
		//{
		//    throw new NotImplementedException();
		//}

		//protected override IStateContainer newStateContainer(object content)
		//{
		//    throw new NotImplementedException();
		//}

		//protected override ITransition newTransition(IStateContainer st, object tr)
		//{
		//    throw new NotImplementedException();
		//}
		//#endregion
    	
    		
		public override InterfaceAutomaton.IA_State DestinationOf (InterfaceAutomaton.IA_Step t)
		{
			return t.Destination;
		}
	}
}
